(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : X ?1 : P (f i c) ?2 : D ∞ _23 : Size [ at Issue2881.agda:21,7-23 ] _25 : D ∞ [ at Issue2881.agda:21,7-23 ] _26 : D ∞ [ at Issue2881.agda:21,7-23 ] _27 : Q (f ∞ ?2) (h ∞ ?2) [ at Issue2881.agda:21,22-23 ] _28 : Q (f ∞ n) (h ∞ n) [ at Issue2881.agda:21,7-23 ] _29 : Q (f ∞ n) (h ∞ n) [ at Issue2881.agda:21,7-23 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _28 := λ n → _27 (n = n) [blocked on problem 51] [51] _25 := λ n → ?2 (n = n) [blocked on problem 52] [51] _23 := λ n → ∞ [blocked on problem 52] [51, 52] f ∞ ?2 = f ∞ n : X [51, 53] h ∞ ?2 = h ∞ n : P (f ∞ _26) " nil)
((last . 1) . (agda2-goals-action '(0 1 2)))
(agda2-status-action "")
(agda2-info-action "*Constraints*" "_28 := λ n → _27 (n = n) [blocked by problem 51] [51] _25 := λ n → ?2 (n = n) [blocked by problem 52] [51] _23 := λ n → ∞ [blocked by problem 52] [51,52] (f ∞ ?2) = (f ∞ n) : X [51,53] (h ∞ ?2) = (h ∞ n) : P (f ∞ _26) " nil)
